Lambda the Ultimate

I am extremely busy (and tired), but what's your excuse for not posting? :-)

Last chance to post something cool before the holidays...

Chickenfoot is a tool that puts a programming environment in Firefox so you can write scripts to manipulate web pages and automate web browsing. In Chickenfoot, scripts are written in a superset of Javascript that includes special functions specific to web tasks.

Chickenfoot is similar to Greasemonkey, but tries to provide a higher level abstraction of web pages, more appropriate for end-user programming.

Take a look at the examples and decide for yourself.

One of the cool things about Second Life is that players can create new kinds of objects, by writing small programs in a special scripting language to describe how the objects should behave, and then launching objects into the world.

Things got really out of hand when the W-Hats created a doomsday device. It looked like a harmless little orb, but it was programmed to make copies of itself, repeatedly. The single object split into two. Then each of those split, and there were four. Then eight, and sixteen, and so on to infinity.

A highly amusing story this is.

I guess the correct term for this kind of thing is The law of unintended DSL consequences.

Please share similar stories, if you got them.

I was dusting off my old copy of "The AWK Programming Language" by Aho, Weinberger and Kernighan (IMHO, one of the best programming books ever written) and decided to see what was being done with AWK these days.

A very interesting networking extension has been added to gawk called Gawkinet. What is particularly interesting is how they managed to add networking capabilities to the language by introducing one new operator "|&" and treating network addresses like files. Leading to examples like:

     
BEGIN {
       "/inet/tcp/0/localhost/daytime" |& getline
       print $0
       close("/inet/tcp/0/localhost/daytime")
     }

Interesting...

Here is a very interesting article addressing a well known compiler problem.

Date: Mon, 12 Dec 2005 17:03:54 -0500
From: David A. Wheeler 
To: bugtraq@securityfocus.com
Subject: Countering Trusting Trust through Diverse Double-Compiling

Everyone here should be familiar with Ken Thompson's famous
"Reflections on Trusting Trust." If not, see:
 http://www.acm.org/classics/sep95/
The "trusting trust" attack subverts the compiler binary;
if attacker succeeds, you're doomed. Well, til now.

I've written a paper on an approach to counter this attack. See:
 "Countering Trusting Trust through Diverse Double-Compiling"
 http://www.acsa-admin.org/2005/abstracts/47.html

Here's the abstract:
"An Air Force evaluation of Multics, and Ken Thompson's famous Turing award
lecture "Reflections on Trusting Trust," showed that compilers can be subverted
to insert malicious Trojan horses into critical software, including themselves.
If this attack goes undetected, even complete analysis of a system's source code
will not find the malicious code that is running, and methods for detecting this
particular attack are not widely known. This paper describes a practical
technique, termed diverse double-compiling (DDC),
that detects this attack and some unintended compiler defects as well.
Simply recompile the purported source code twice: once with a second (trusted)
compiler, and again using the result of the first compilation.
If the result is bit-for-bit identical with the untrusted
binary, then the source code accurately represents the binary.
This technique has been mentioned informally, but its issues and
ramifications have not been identified or discussed in a
peer-reviewed work, nor has a public demonstration been made.
This paper describes the technique, justifies it, describes how
to overcome practical challenges, and demonstrates it."

I think you'll find this interesting.

--- David A. Wheeler

Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the non-functional IO actions ---which do have side effects--- from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge?

This report scratches the surface of category theory, an abstract branch of algebra, just deep enough to find the monad structure. On the way we discuss the relations to the purely functional programming language Haskell. Finally it should become clear how the IO monad keeps Haskell pure.

It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written.

The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory.

The MetaC language extends C in a 100% backward compatible way with reflective features and techniques for refactoring, reconfiguring and modifying arbitrary C source code. Therefore, the extensions provide special metadata types for working with source code information, syntactical structures for the definiton of code templates, and metafunctions to gather information about source code and refactor, modify, delete, or insert code.

by Jérôme Vouillon

We propose a type system based on regular tree grammars, where algebraic datatypes are interpreted in a structural way. Thus, the same constructors can be reused for different types and a flexible subtyping relation can be defined between types, corresponding to the inclusion of their semantics. For instance, one can define a type for lists and a subtype of this type corresponding to lists of even length. Patterns are simply types annotated with binders. This provides a generalization of algebraic patterns with the ability of matching arbitrarily deep in a value. Our main contribution, compared to languages such as XDuce and CDuce, is that we are able to deal with both polymorphism and function types.

It will appear in POPL '06.

Lennart Augustsson announced Djinn on the Haskell mailing list recently.

He included this demonstration:

I've written a small program that takes a (Haskell) type
and gives you back a function of that type if one exists.
It's kind of fun, so I thought I'd share it.

It's probably best explained with a sample session.

   calvin% djinn
   Welcome to Djinn version 2005-12-11.
   Type :h to get help.
# Djinn is interactive if not given any arguments.
# Let's see if it can find the identity function.
   Djinn> f ? a->a
   f :: a -> a
   f x1 = x1
# Yes, that was easy.  Let's try some tuple munging.
   Djinn> sel ? ((a,b),(c,d)) -> (b,c)
   sel :: ((a, b), (c, d)) -> (b, c)
   sel ((_, v5), (v6, _)) = (v5, v6)

# We can ask for the impossible, but then we get what we
# deserve.
   Djinn> cast ? a->b
   -- cast cannot be realized.

# OK, let's be bold and try some functions that are tricky to write:
# return, bind, and callCC in the continuation monad
   Djinn> type C a = (a -> r) -> r
   Djinn> returnC ? a -> C a
   returnC :: a -> C a
   returnC x1 x2 = x2 x1

   Djinn> bindC ? C a -> (a -> C b) -> C b
   bindC :: C a -> (a -> C b) -> C b
   bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))

   Djinn> callCC ? ((a -> C b) -> C a) -> C a
   callCC :: ((a -> C b) -> C a) -> C a
   callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11)
# Well, poor Djinn has a sweaty brow after deducing the code
# for callCC so we had better quit.
   Djinn> :q
   Bye.

To play with Djinn do a
darcs get http://darcs.augustsson.net/Darcs/Djinn
or get
http://darcs.augustsson.net/Darcs/Djinn/Djinn.tar.gz
Then just type make. (You need a Haskell 98 implementation and
some libraries.) And then start djinn.

For the curious, Djinn uses a decision procedure for intuitionistic
propositional calculus due to Roy Dyckhoff. It's a variation of
Gentzen's LJ system. This means that (in theory) Djinn will always
find a function if one exists, and if one doesn't exist Djinn will
terminate telling you so.

This is the very first version, so expect bugs. :)

Don Stewart wrote a lambdabot plugin for Djinn a few hours later.

15:39:01  @djinn a -> b -> a
15:39:02  x :: a -> b -> a
15:39:02  x x1 _ = x1
15:39:11  @djinn (a -> b -> c) -> ((a,b) -> c)
15:39:11  x :: (a -> b -> c) -> (a, b) -> c
15:39:11  x x1 (v3, v4) = x1 v3 v4
15:39:27  @djinn (a -> b) -> (c -> b) -> Either a c -> b
15:39:27  x :: (a -> b) -> (c -> b) -> Either a c -> b
15:39:27  x x1 x2 x3 = case x3 of
15:39:27       Left l4 -> x1 l4
15:39:27       Right r5 -> x2 r5
15:40:06  @djinn a -> [a] -> [a]
15:40:07  x :: a -> [a] -> [a]
15:40:07  x _ x2 = x2
15:40:08  @help djinn
15:40:09   @djinn 
15:40:09  Generates Haskell code from a type.

Djinn has proven to be much fun on #haskell.

2005 is nearly over, and as everyone knows, December is the time for compiling hugely subjective Top 5 (10, 20, 100) lists for everything under the sun. I think it would be fun to see everybody's favorite papers... Here's mine, totally off the top of my head (I'm sure I'm forgetting something essential):

• Scalable Component Abstractions - Martin Odersky and Matthias Zenger
• Generic implementation of all four *F* operators: from control0 to shift - Oleg Kiselyov
• Composable Memory Transactions - Tim Harris, Simon Marlow, Simon Peyton Jones, and Maurice Herlihy
• Putting Curry-Howard to Work - Tim Sheard
• Extensible Records With Scoped Labels - Daan Leijen

(Don't worry about trying to post the "best" papers in some objective sense, just whatever excited you... Show me what I missed this year!)